#include "symbolics.h"
#include <iostream>
#include <fstream>
#include <cstdlib>//abort
#include <iomanip>//hexa stuff

namespace divine {

//---------Node----------
Node::Node(): arity( 0 ) {}

Node::Node( int n ): arity( n ) {
  heirs.resize( n );
}

Node::Node( TYPE t, OPTYPE o, int ar, uint32_t one, uint32_t two ) {
  type = t;
  op = o;
  arity = ar;
  heirs.push_back( one );
  if ( arity > 1 )
    heirs.push_back( two );
}

Node::Node( TYPE t, uint32_t _name ) : arity( 0 ) {
  if ( t == VAR ) {
    type = VAR;
    name = _name;
  }
  else {
    type = CON;
    value = _name;
  }
}
 
Node::Node( const Node &n ) {
  type = n.type;
  op = n.op;
  arity = n.arity;
  name = n.name;
  round = n.round;
  value = n.value;
  heirs = n.heirs;
}

//next 3 functions are for blobbing
int Node::size() {
  int retVal = 0;
  retVal += sizeof( TYPE );
  retVal += sizeof( OPTYPE );
  retVal += 16;
  retVal += 4 * heirs.size();
  return retVal;
}

void Node::rebuild( char **tab ) {
  blobRead< TYPE >( &type, tab );
  blobRead< OPTYPE >( &op, tab );
  blobRead< int >( &arity, tab );
  blobRead< int >( &name, tab );
  blobRead< int >( &round, tab );
  blobRead< uint32_t >( &value, tab );
  if ( arity != 0 && type != OP ) {//debug
    std::cerr << "Error: wrong node read." << std::endl;
    print( "rebuild" );
    abort();
  }
  heirs.resize( arity );
  for ( int i = 0; i < arity; i++ ) {
    blobRead< uint32_t >( &(heirs.at( i )), tab );
  }
}

void Node::store( char **tab ) {
  blobWrite< TYPE >( tab, &type );
  blobWrite< OPTYPE >( tab, &op );
  blobWrite< int >( tab, &arity );
  blobWrite< int >( tab, &name );
  blobWrite< int >( tab, &round );
  blobWrite< uint32_t >( tab, &value );
  for ( int i = 0; i < arity; i++ ) {
    blobWrite< uint32_t >( tab, &(heirs.at( i )) );
  }
}

//debug
void Node::print( std::string s ) {
  std::cout << s << ": [" << type << "|" << op << "|" << arity << "|"
            << name << "|" << round << "|" << value;
  if ( heirs.size() > 0 )
    std::cout << "|" << heirs.at( 0 );
  if ( heirs.size() > 1 )
    std::cout << "|" << heirs.at( 1 );
  std::cout << "]" << std::endl;
}
//---------Node-----------
 
//----------Expr----------
Expr::Expr( SMTRep *_smt ): smt( _smt ) {}

Expr::Expr( Expr &e ) {
  nodes = e.nodes;
  smt = e.smt;
}

Expr::Expr( const Expr &e ) {
  nodes = e.nodes;
  smt = e.smt;
}

Expr::Expr( Expr *e ) {
  nodes = e->nodes;
  smt = e->smt;
}

//debug
bool Expr::check_sanity() {
  for ( int i = 0; i < nodes.size(); i++ ) {
    for ( int j = 0; j < nodes.at( i ).heirs.size(); j++ ) {
      if ( nodes.at( i ).heirs.at( j ) == i ) {
        std::cerr << "Wrong expression." << std::endl;
        abort();
      }
    }
  }
}
 
//special function for inport variables
//new round requires new set of them
void Expr::round( int r ) {
  for ( int i = 0; i < nodes.size(); i++ )
    if ( nodes.at( i ).type == VAR )
      nodes.at( i ).round = r;
}

//substitute every variables named $order$ with the expression $*e$
//now only used in addToPath
void Expr::subs( int order, Expr *e ) {
  std::vector< int > holders;
  //first find out if there are any such named variables
  //and remember their positions
  for ( int i = 0; i < nodes.size(); i++ ) {
    if ( nodes.at( i ).type == VAR && nodes.at( i ).name == order )
      holders.push_back( i );
  }
  if ( holders.empty() )
    return;

  //update a copy of the expression "e", so that the individual nodes
  //point to resulting positions (increase by size of this expression)
  std::vector< Node > tempVe = e->nodes;
  for ( int j = 0; j < tempVe.size(); j++ )
    for ( int i = 0; i < tempVe.at( j ).heirs.size(); i++ )
      tempVe.at( j ).heirs.at( i ) += nodes.size() - 1;

  //copy over each node, bar the root
  if ( tempVe.size() == 0 )
    abort();
  for ( int i = 1; i != tempVe.size(); i++ )
    nodes.push_back( tempVe.at( i ) );

  //replace the root (of e) for every stored position
  for ( int i = 0; i < holders.size(); i++ ) {
    nodes.at( holders.at( i ) ) = tempVe.at( 0 );
  }
}

//main AST to SMT2 translating function
//does little but tran is already recursive (have to start somewhere)
std::string Expr::translate( bool B, std::string name ) {
  if ( nodes.size() == 0 )
    return "";
  return tran( 0, B, name );
}

//debug
std::string Expr::print() {
  std::stringstream s;
  for ( int i = 0; i < nodes.size(); i++ ) {
    s << i << "|" << nodes.at( i ).type  << ": ";
    for ( int j = 0; j < nodes.at( i ).heirs.size(); j++ ) {
      s << nodes.at( i ).heirs.at( j ) << " ";
    }
    s << std::endl;
  }
  return s.str();
}

//explicit conversion for SMT2's strong type system
std::string Expr::convert( uint32_t val, bool Bool ) {
  std::stringstream str;
  if ( Bool )
    return (val ? "true" : "false");
  str << "#x" << std::setfill( '0' ) << std::setw( bit_width / 4 )
      << std::hex << val;
  return str.str();
}

//same as above but with variables
std::string Expr::convert( std::string val, bool Bool ) {
  if ( !Bool )
    return val;
  std::stringstream str;
  str << "(= " << val << " #x" << std::setfill( '0' )
      << std::setw( bit_width / 4 ) << std::hex << 1 << ")";
  return str.str();
}

//translate one node (on index $i$), $Bool$ if we expect it to be Boolean
//$name$ is the template name for variables (other then this, they are numbered)
std::string Expr::tran( uint32_t i, bool Bool, std::string name ) {
  Node n = nodes.at( i );
  //first sort out some debugging
  if ( n.arity > 0 && n.heirs.at( 0 ) == i )
    abort();
  if ( n.arity > 1 && n.heirs.at( 1 ) == i )
    abort();
  if ( n.arity > 2 && n.heirs.at( 2 ) == i )
    abort();
  //now deal with atoms
  if ( n.arity == 0 ) {
    std::stringstream s, str;
    switch ( n.type ) {
    case CON :
      s << " " << convert( n.value, Bool );
      break;
    case VAR :
      str << name << n.name << "x" << n.round;
      s << " " << convert( str.str(), Bool );
      break;
    }
    return s.str();
  }
  
  std::string first, second, third;
  std::stringstream temp;
  
  //list of operators may be incomplete
  switch ( n.op ) {
  case MIN : //so far only two
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(ite (bvult" + first + second + ") " + first + " " + second
      + ")";
  case MAX : //so far only two
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(ite (bvugt" + first + second + ") " + first + " " + second
      + ")";
  case SWITCH :
    //funny semantics, taken from simulink.h
    first = tran( n.heirs.at( 0 ), Bool, name );
    second = tran( n.heirs.at( 1 ), true, name );
    third = tran( n.heirs.at( 2 ), Bool, name );
    return "(ite " + second + " " + first + " " + third + ")";
  case LT :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvult" + first + second + ")";
  case LE :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvule" + first + second + ")";
  case GT :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvugt" + first + second + ")";
  case GE :
    //TODO - rewrite the other comparators as well
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    if ( Bool )
      return "(bvuge" + first + second + ")";
    temp << "(ite (bvuge" << first << second << ") " << convert( 1, false )
         << " " << convert( 0, false ) << ")";
    return temp.str();
  case NEQ :
    first = tran( n.heirs.at( 0 ), Bool, name );
    second = tran( n.heirs.at( 1 ), Bool, name );
    return "(distinct" + first + second + ")";
  case EQ :
    first = tran( n.heirs.at( 0 ), Bool, name );
    second = tran( n.heirs.at( 1 ), Bool, name );
    return "(=" + first + second + ")";
  case NOT :
    first = tran( n.heirs.at( 0 ), true, name );
    return "(not" + first + ")";
  case AND :
    first = tran( n.heirs.at( 0 ), true, name );
    second = tran( n.heirs.at( 1 ), true, name );
    return "(and" + first + second + ")";
  case OR :
    //TODO - rewrite other Boolean operators
    first = tran( n.heirs.at( 0 ), true, name );
    second = tran( n.heirs.at( 1 ), true, name );
    if ( Bool )
      return "(or" + first + second + ")";
    temp << "(ite (or" << first << second << ") " << convert( 1, false )
         << " " << convert( 0, false ) << ")";
    return temp.str();
  case IMP :
    first = tran( n.heirs.at( 0 ), true, name );
    second = tran( n.heirs.at( 1 ), true, name );
    return "(=>" + first + second + ")";
  case XOR :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvxnor" + first + second + ")"; //???
  case NAND :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvnand" + first + second + ")";
  case NOR :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    return "(bvnor" + first + second + ")";
  case PLUS :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    if ( Bool ) {
      return "(distinct (bvadd" + first + second + ") "
        + convert( 0, false ) + ")";
    }
    return "(bvadd" + first + second + ")";
  case TIMES :
    first = tran( n.heirs.at( 0 ), false, name );
    second = tran( n.heirs.at( 1 ), false, name );
    if ( Bool ) {
      return "(distinct (bvmul" + first + second + ") "
        + convert( 0, false ) + ")";
    }
    return "(bvmul" + first + second + ")";
  case CAST :
    first = tran( n.heirs.at( 0 ), true, name );
    if ( Bool )
      return first;
    return "(ite " + first + " " + convert( 1, false ) + " "
      + convert( 0, false ) + ")";
  default :
    std::cerr << "Error: Unknown literal." << std::endl;
    abort();
  }
}

void Expr::clear() {
  root = 0;
  nodes.clear();
}

//more blobbing
int Expr::size() {
  int retVal = 0;
  retVal += 4;
  for ( int i = 0; i < nodes.size(); i++ )
    retVal += nodes.at( i ).size();
  return retVal;
}

void Expr::rebuild( char **tab ) {
  int nodes_size;
  blobRead< int >( &nodes_size, tab );
  nodes.resize( nodes_size );
  for ( int i = 0; i < nodes.size(); i++ )
    nodes.at( i ).rebuild( tab );
}

void Expr::store( char **tab ) {
  int nodes_size = nodes.size();
  blobWrite< int >( tab, &(nodes_size) );
  for ( int i = 0; i < nodes.size(); i++ )
    nodes.at( i ).store( tab );
}
//----------Expr----------

//--------SMTRep-------------
SMTRep::SMTRep() {
  //counter = 0;//debug
  //times.resize( 16 );//debug
  cond_tick = false;
  pc.push_back( Expr( this ) );
}

SMTRep::SMTRep( SMTRep *r ) {
  os = r->os;
  offset = r->offset;
  //counter = r->counter;//debug
  //times = r->times;//debug
  pc = r->pc;
}

//tick of the global clocks
void SMTRep::tick() {
  //tick might render pc unsatisfiable
  //we do proper tick once we know pc is sat
  if ( cond_tick )
    return;
  cond_tick = true;
  // if ( round > 15 ) {//debug
  //   for ( int i = 0; i < times.size(); i++ ) {
  //     std::cout << i << " " << times.at( i ).checks << " "
  //               << times.at( i ).time << " "
  //               << times.at( i ).size << " "
  //               << times.at( i ).state_size << " "
  //               << times.at( i ).assertions << std::endl;
  //   }
  //   abort();//debug
  // }
  //std::cout << "tick " << round << std::endl;

  Expr e( this );
  Node n( CON, 1 );
  e.nodes.push_back( n );
  pc.push_back( e );
}

//hopefully last blobbing
int SMTRep::size() {
  int retVal = 8;
  retVal += sizeof(int); //in_val_size
  retVal += in_values.size() * sizeof(uint32_t);
  retVal += sizeof(int); //pc_size
  for ( int i = 0; i < pc.size(); i++ ) {
    retVal += pc.at( i ).size();
  }
  return retVal;
}

void SMTRep::read( char *tab ) {
  char *table = tab;
  table += 8;
  int in_values_size;
  blobRead< int >( &(in_values_size), &(table) );
  in_values.resize( in_values_size );
  for ( int i = 0; i < in_values_size; i++ ) {
    blobRead< uint32_t >( &(in_values.at( i )), &(table) );
  }
  int pc_size;
  blobRead< int >( &(pc_size), &(table) );
  if ( pc_size == 0 ) {//debug
    std::cerr << "Error: wrong pc size." << std::endl;
    abort();
  }
  pc.resize( pc_size );
  for ( int i = 0; i < pc_size; i++ ) {
    pc.at( i ).smt = this;
    pc.at( i ).rebuild( &(table) );
  }
}

void SMTRep::write( char *tab ) {
  char *table = tab;
  table += (8 - sizeof(SMTRep*));
  SMTRep *r = this;
  //guess how will the hash table know how to talk to SMT solver
  blobWrite< SMTRep* >( &(table), &(r) );
  int in_values_size = in_values.size();
  blobWrite< int >( &(table), &(in_values_size) );
  for ( int i = 0; i < in_values_size; i++ ) {
    blobWrite< uint32_t >( &(table), &(in_values.at( i )) );
  }
  int pc_size = pc.size();
  blobWrite< int >( &(table), &(pc_size) );
  if ( pc_size == 0 ) {//debug
    std::cerr << "Error: wrong pc size." << std::endl;
    abort();
  }
  for ( int i = 0; i < pc_size; i++ ) {
    pc.at( i ).store( &(table) );
  }
}

//probably for labels
std::string SMTRep::print() {
  std::stringstream s;
  s << "---------------------------" << std::endl;
  s << "[";
  for ( int i = 0; i < in_values.size(); i++ )
    s << in_values.at( i ) << " ";
  s << "]" << std::endl;
  s << "-----------" << std::endl;
  s << "<";
  for ( int i = 0; i < pc.size(); i++ )
    s << pc.at( i ).translate( false, "a" ) << " ";
  s << ">" << std::endl;
  s << "---------------------------";
  return s.str();
}

//same as in Expr
std::string SMTRep::convert( uint32_t val, bool Bool ) {
  std::stringstream str;
  if ( Bool )
    return (val ? "true" : "false");
  str << "#x" << std::setfill( '0' ) << std::setw( bit_width / 4 )
      << std::hex << val;
  return str.str();
}

//nasty linear search through the known variables,
//doesn't happen too often and there's only a few of them
int SMTRep::by_name( std::string n ) {
  for ( int i = 0; i < os.size(); i++ )
    if ( os.at( i ).s == n )
      return i;
  abort();
}

//check satisfiability of the current path condition
//$last$ is true if we have all sub path conditions
bool SMTRep::pc_sat( bool last ) {
  //times.at( round ).checks++;//debug
  startTimer();
  std::ofstream smt_input;
  smt_input.open("/home/xhavel1/Paradise/ceds/z3_divine/in.smt2");
  smt_input << "(set-option :produce-models true)\n";
  smt_input << "(set-logic BV)\n";
  //declare all variables
  for ( int i = 0; i < pc.size(); i++ )
    for ( int j = 0; j < os.size(); j++ )
      smt_input << "(declare-fun a" << j << "x" << i
                << " () (_ BitVec " << bit_width << "))\n";

  //define semantics of variables, given original expressions
  Expr e;
  for ( int i = 0; i < pc.size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ ) {
      //delays are zero in first round
      if ( i == 0 && os.at( j ).d == DEL ) {
        smt_input << "(assert (= a" << j << "x" << 0
                  << " " << convert( 0, false ) << "))\n";
        continue;
      }
      e = os.at( j ).e;
      e.round( i );
      //inports are simple always assertions
      smt_input << "\n";
      if ( os.at( j ).d == INP ) {
        smt_input << "(assert " << e.translate( true, "a" ) << ")\n";
        continue;
      }
      //outports always and delays for round > 0
      smt_input << "(assert (= a" << j << "x" << i << " "
                << e.translate( false, "a" ) << "))\n";
    }
  }
    
  //write down the assertion making up the pc - one for every round
  for ( int i = 0; i < pc.size(); i++ ) {
    if ( pc.at( i ).nodes.empty() ) {
      Node n( CON, 1 );
      pc.at( i ).nodes.push_back( n );
    }
    //std::cout << "pc at " << i << " is " << pc.at( i ).translate( true, "a" ) << std::endl;//debug
    smt_input << "(assert " + pc.at( i ).translate( true, "a" ) + ")\n";
  }

  //limit inports to read at most k distinct values
  smt_input << "(define-sort Full () (_ BitVec " << bit_width << "))\n";
  smt_input << "(assert (exists (";
  for ( int l = 0; l < distinct_invalues; l++ ) {
    smt_input << "(lim" << l << " Full)";
  }
  smt_input << ") (and ";
  for ( int j = 0; j < os.size(); j++ ) {
    if ( os.at( j ).d == INP ) {
      for ( int i = 0; i < pc.size(); i++ ) {
        smt_input << "(or ";
        for ( int l = 0; l < distinct_invalues; l++ ) {
            smt_input << "(= a" << j << "x" << i << " lim" << l << ")";
        }
        smt_input << ")";
      }
    }
  }
  smt_input << ")))\n";

  smt_input << "(check-sat)\n";
  //we need the last round for counterexample
  smt_input << "(get-value (";
  for ( int i = 0; i < os.size(); i++ ) {
    if ( os.at( i ).d != INP )
      continue;
    smt_input << "a" << i << "x" << pc.size() - 1 << " ";
  }
  smt_input << "))\n";
  smt_input.close();
  //debug->
  //std::ifstream file( "in.smt2", std::ios::binary | std::ios::ate );
  //times.at( round ).size += file.tellg();
  //file.close();
  //times.at( round ).assertions += pc.size();
  //<-debug
  //call the smt solver
  system( "/home/xbauch/z3/build/z3 -smt2 /home/xbauch/divines/z3_divine/_build/tools/in.smt2 > /home/xbauch/divines/z3_divine/_build/tools/out.txt" );
  //if ( last ) abort();//debug
  //read the result and if sat, then store the counterexample inports
  std::ifstream smt_output;
  smt_output.open( "out.txt", std::ifstream::in );
  int ch = smt_output.get();
  bool retVal;
  if ( ch == '(' ) {
    std::cerr << "Error: wrong input for SMT." << std::endl;
    abort();
  }
  if ( ch == 'u' ) {
    //std::cout << "unsat" << std::endl;//debug
    retVal = false;
  }
  else {
    //std::cout << "sat" << std::endl;//debug
    char line[ 256 ];
    smt_output.getline( line, 256 );
    //read the lines, parse the hexa values of the generated model
    for ( int i = 0; i < os.size(); i++ ) {
      if ( os.at( i ).d != INP )
        continue;
      smt_output.getline( line, 256 );
      for ( int j = 0; j < 256; j++ ) {
        if ( line[ j ] == '#' ) {
          line[ j ] = '0';
          std::string tempString( line + j, line + j + 4 );
          std::stringstream tempStream;
          tempStream << std::hex << tempString;
          uint32_t tempValue;
          tempStream >> tempValue;
          in_values.push_back( tempValue );
          break;
        }
      }
    }
    retVal = true;
  }
  if ( last ) {
    if ( retVal ) {
      cond_tick = false;
      //times.at( round ).state_size += size();//debug
    }
    else
      pc.back().clear();
  }
  //times.at( round ).time += endTimer();//debug
  return retVal;
}

//called from the buchi automaton (the .inc file)
//add one more assertion to the current path condition
void SMTRep::addToPath( Expr *last ) {
  //pc.at( round ).check_sanity();//debug
  //last->check_sanity();//debug
  if ( pc.back().nodes.empty() )
    pc.back() = *last;
  else {
    //if there already is something form a conjunction
    Expr e( this );
    Node andN( OP, AND, 2, 1, 2 );
    e.nodes.push_back( andN );
    Node vN1( VAR, 0 );
    e.nodes.push_back( vN1 );
    Node vN2( VAR, 1 );
    e.nodes.push_back( vN2 );
    e.subs( 0, &(pc.back()) );
    e.subs( 1, last );
    pc.back() = e;
  }
  pc.back().round( pc.size() - 1 );
  //pc.at( round ).check_sanity();
}

//verify that evaluations satisfying $pc1$ also satisfy $pc2$
//see the paper for more details
bool SMTRep::subseteq( std::vector< Expr > *pc1, std::vector< Expr > *pc2 ) {
  std::ofstream smt_input;
  smt_input.open("/home/xhavel1/Paradise/ceds/z3_divine/in.smt2");
  smt_input << "(set-option :mbqi true)\n";
  smt_input << "(define-sort Full () (_ BitVec " << bit_width << "))\n";
  //declare the variables
  for ( int i = 0; i < pc1->size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ )
      smt_input << "(declare-fun a" << j << "x" << i
                << " () (_ BitVec " << bit_width << "))\n";
  }
  for ( int i = 0; i < pc2->size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ ) {
      if ( os.at( j ).d == INP )
        continue;
      smt_input << "(declare-fun b" << j << "x" << i
                << " () (_ BitVec " << bit_width << "))\n";
    }
  }

  Expr e;
  for ( int i = 0; i < pc1->size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ ) {
      //delays are zero in first round
      if ( i == 0 && os.at( j ).d == DEL ) {
        smt_input << "(assert (= a" << j << "x" << 0
                  << " " << convert( 0, false ) << "))\n";
        continue;
      }
      e = os.at( j ).e;
      e.round( i );
      //inports are simple always assertions
      if ( os.at( j ).d == INP ) {
        smt_input << "(assert " << e.translate( true, "a" ) << ")\n";
        continue;
      }
      //outports always and delays for round > 0
      smt_input << "(assert (= a" << j << "x" << i << " "
                << e.translate( false, "a" ) << "))\n";
    }
  }
  //limit inports to read at most k distinct values
  smt_input << "(assert (exists (";
  for ( int l = 0; l < distinct_invalues; l++ ) {
    smt_input << "(lim" << l << " Full)";
  }
  smt_input << ") (and ";
  for ( int j = 0; j < os.size(); j++ ) {
    if ( os.at( j ).d == INP ) {
      for ( int i = 0; i < pc1->size(); i++ ) {
        smt_input << "(or ";
        for ( int l = 0; l < distinct_invalues; l++ ) {
            smt_input << "(= a" << j << "x" << i << " lim" << l << ")";
        }
        smt_input << ")";
      }
    }
  }
  smt_input << ")))\n";
  
  //write down the assertion making up the pcs
  for ( int i = 0; i < pc1->size(); i++ ) {
    if ( pc1->at( i ).nodes.empty() ) {
      Node n( CON, 1 );
      pc1->at( i ).nodes.push_back( n );
    }
    smt_input << "(assert " + pc1->at( i ).translate( true, "a" ) + ")\n";
  }

  smt_input << "(assert (forall (";
  for ( int i = 0; i < pc2->size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ ) {
      if ( os.at( j ).d != INP )
        continue;
      smt_input << "(b" << j << "x" << i << " Full)";
    }
  }
  smt_input << ") (=> (and ";
  for ( int i = 0; i < pc2->size(); i++ ) {
    for ( int j = 0; j < os.size(); j++ ) {
      //delays are zero in first round
      if ( i == 0 && os.at( j ).d == DEL ) {
        smt_input << "(= b" << j << "x" << 0
                  << " " << convert( 0, false ) << ") ";
        continue;
      }
      e = os.at( j ).e;
      e.round( i );
      //inports are simple always assertions
      if ( os.at( j ).d == INP ) {
        smt_input << e.translate( true, "b" ) << " ";
        continue;
      }
      //outports always and delays for round > 0
      smt_input << "(= b" << j << "x" << i << " "
                << e.translate( false, "b" ) << ") ";
    }
  }
  for ( int i = 0; i < pc2->size(); i++ ) {
    if ( pc2->at( i ).nodes.empty() ) {
      Node n( CON, 1 );
      pc2->at( i ).nodes.push_back( n );
    }
    smt_input << pc2->at( i ).translate( true, "b" );
  }
  smt_input << ") (or ";
  for ( int i = 0; i < os.size(); i++ ) {
    if ( os.at( i ).d != DEL )
      continue;
    smt_input << "(distinct a" << i << "x" << pc1->size() - 1
              << " b" << i << "x" << pc2->size() - 1 << ")";
  }
  smt_input << "))))\n";
  smt_input << "(check-sat)\n";
  smt_input.close();
  //abort();
  system( "/home/xbauch/z3/build/z3 -smt2 /home/xbauch/divines/z3_divine/_build/tools/in.smt2 > /home/xbauch/divines/z3_divine/_build/tools/out.txt" );
  //abort();//debug
  //read the result
  std::ifstream smt_output;
  smt_output.open( "out.txt", std::ifstream::in );
  int ch = smt_output.get();
  if ( ch == '(' ) {
    std::cerr << "Error: wrong input for smt." << std::endl;
    abort();
  }
  if ( ch == 's' ) {
    return true;
  }
  else {
    return false;
  }
}

//external functions to be called from hashset
bool SMTRep::check_ide( std::vector< Expr > *pc1, std::vector< Expr > *pc2 ) {
  bool retVal;
  //return true;//debug
  //Idea: could be easily run in parallel
  retVal = (subseteq( pc1, pc2 ) || subseteq( pc2, pc1 ));
  if ( retVal )//debug
    std::cout << "distinct." << std::endl;
  else
    std::cout << "equal." << std::endl;
  return !retVal;
}

int SMTRep::find( std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  for ( int i = 0; i < pcs->size(); i++ )
    if ( check_ide( &(pcs->at( i )), &(pc) ) )
      return i;
  return pcs->size();
}

bool SMTRep::has( std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  for ( int i = 0; i < pcs->size(); i++ )
    if ( check_ide( &(pcs->at( i )), &(pc) ) )
      return true;
  return false;
}

int SMTRep::addIfNew( std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  for ( int i = 0; i < pcs->size(); i++ )
    if ( check_ide( &(pcs->at( i )), &(pc) ) )
      return i;
  pcs->push_back( pc );
  return -1;
}

void SMTRep::add( std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  pcs->push_back( pc );
}

}
